/*
 * SplittingTreeTest.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <gtest/gtest.h>

#include <iostream>
#include <fstream>

#include "bfr/Clause.hpp"
#include "bfr/ClauseSet.hpp"
#include "bfr/OccurrencePattern.hpp"
#include "bfr/DIMACSParser.hpp"

#include "bfr/lpbCombinatorial/SplittingTree.hpp"
#include "bfr/lpbCombinatorial/SplittingTreeNode.hpp"

namespace bfr { namespace test {

TEST(SplittingTree, createTree) {
    DIMACSParser parser;
    std::ifstream in;
    in.open("test_files/lpb_ex1.dnf");
    ClauseSet *dnf = parser.parse(in);
    SplittingTree t(dnf, 3);
    t.createTree(true ,false);
    in.close();

    // check if it creates the DNFs correctly
    // COLUMN 1
    ClauseSet *r10 = new ClauseSet(1);
    Clause *r101 = new Clause(2);
    r101->addSecure(new Literal(1));
    r101->addSecure(new Literal(2));
    r10->addSecure(r101);

    ClauseSet *r11 = new ClauseSet(1);
    Clause *r111 = new Clause(0);
    r11->addSecure(r111);

    SplittingTreeNode *root = t.getRoot();
    SplittingTreeNode *n10 = root->getUpperChild();
    SplittingTreeNode *n11 = root->getLowerChild();
    EXPECT_EQ(*(n10->getDNF()), *r10);
    EXPECT_EQ(*(n11->getDNF()), *r11);

    // COLUMN 2
    ClauseSet *r20 = new ClauseSet(0);

    ClauseSet *r21 = new ClauseSet(1);
    Clause *r211 = new Clause(1);
    r211->addSecure(new Literal(2));
    r21->addSecure(r211);

    SplittingTreeNode *n20 = n10->getUpperChild();
    SplittingTreeNode *n21 = n10->getLowerChild();

    EXPECT_EQ(*(n20->getDNF()), *r20);
    EXPECT_EQ(*(n21->getDNF()), *r21);

    // COLUMN 3
    SplittingTreeNode *n30 = n20->getUpperChild();
    SplittingTreeNode *n31 = n20->getUpperChild();
    SplittingTreeNode *n32 = n21->getLowerChild();

    // they should share the DNF
    EXPECT_EQ(n20->getLowerChild(), n21->getUpperChild());

    EXPECT_EQ(*(n30->getDNF()), *r20);
    EXPECT_EQ(*(n31->getDNF()), *r20);
    EXPECT_EQ(*(n32->getDNF()), *r11);

    delete r10;
    delete r11;
    delete r20;
    delete r21;
}

}}

